r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a).
(w:|r|. SqStable(a(w)))  (v:|r|. ((d(v)))  (a(v))) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, Ideal(r){i}
Definitions	, t  T, P  Q, x:A. B(x), P & Q, P  Q, P  Q, True, T, Rng, Ideal(r){i}, CRng, detach_fun(T;A), SqStable(P), {T}
Lemmas	crng wf, ideal wf, detach fun wf, sq stable wf, rng car wf, squash elim, squash wf, assert wf, iff functionality wrt iff, sq stable squash, decidable assert, sq stable from decidable, sq stable iff, detach fun properties, iff symmetry